\begin{tabbing}
EventsWithValues\{i\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$E$:Type\{i\}\+
\\[0ex]$\times$ (${\it eq}$:EqDecider($E$)
\\[0ex]$\times$ ${\it pred?}$:($E$$\rightarrow$($E$ + Unit))
\\[0ex]$\times$ ${\it info}$:($E$$\rightarrow$((:Id $\times$ Id) + (:(:IdLnk $\times$ $E$) $\times$ Id)))
\\[0ex]$\times$ ${\it oaxioms}$:EO\=rderAxioms\{i\}($E$;\+
\\[0ex]${\it pred?}$;
\\[0ex]${\it info}$)
\-\\[0ex]$\times$ $T$:(Id$\rightarrow$Id$\rightarrow$Type\{i\})
\\[0ex]$\times$ ${\it when}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc(${\it info}$;$e$),$x$))
\\[0ex]$\times$ ${\it after}$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc(${\it info}$;$e$),$x$))
\\[0ex]$\times$ ${\it saxiom}$:\=($\forall$$e$:$E$.\+
\\[0ex]($\neg$($\uparrow$first(${\it pred?}$;$e$)))
\\[0ex]$\Rightarrow$ ($\forall$$x$:Id. ${\it when}$($x$,$e$) = ${\it after}$($x$,pred(${\it pred?}$;$e$)) $\in$ $T$(loc(${\it info}$;$e$),$x$)))
\-\\[0ex]$\times$ $V$:(Knd$\rightarrow$Id$\rightarrow$Type\{i\})
\\[0ex]$\times$ (${\it val}$:($e$:$E$$\rightarrow$$V$(kind(${\it info}$;$e$),loc(${\it info}$;$e$)))
\\[0ex]$\times$ Top))
\-
\end{tabbing}